(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 3.
The certificate found is represented by the following graph.
Start state: 301
Accept states: [302, 303]
Transitions:
301→302[a_1|0]
301→303[c_1|0]
301→301[b_1|0]
301→304[a_1|1]
301→305[a_1|2]
301→306[c_1|2]
304→305[a_1|1]
304→306[c_1|2]
305→306[c_1|1]
306→307[a_1|1]
306→302[b_1|2]
306→304[b_1|2]
306→305[b_1|2]
306→308[a_1|2]
306→309[a_1|2, a_1|3]
306→310[c_1|3, c_1|2]
307→302[b_1|1]
307→304[b_1|1]
307→305[b_1|1]
307→308[a_1|2]
307→309[a_1|3]
307→310[c_1|3]
308→309[a_1|2]
308→310[c_1|3]
309→310[c_1|2]
310→311[a_1|2]
310→305[b_1|3]
311→305[b_1|2]